A:Type, B:(AType), eq:EqDecider(A), f,g:fpf(A; a.B(a)).
fpf-compatible(A; a.B(a); eq; f; g)  fpf-sub(A; a.B(a); eq; g; fpf-join(eq; f; g)) 

latex

Definitions	x:A. B(x), x(s), P  Q, fpf-sub(A; a.B(a); eq; f; g), A c B, P  Q, P  Q, P  Q, t  T, x. t(x), P  Q, guard(T), prop{i:l}, if b then t else f fi , tt, ff, , Unit, fpf-compatible(A; a.B(a); eq; f; g),
Lemmas	fpf-join-dom, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-ap wf, fpf-join-ap, bool wf, eqtt to assert, iff transitivity, bnot wf, not wf, eqff to assert, assert of bnot, fpf-compatible wf, fpf wf, deq wf